Inference at * 1 1 1 1 
Iof proof for Lemma before-hd:



1. T : Type
2. L : T List
3. 0 < ||L||
4. no_repeats(T;L)
5. x : T
6. x before hd(L)  L
7. x, y:T. x before y  L  ((x = y))
8. (x = hd(L))
9. hd(L) before x  L
10. x before x  L
11. (x = x)
  False 

latex

 by ((D (-1)) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

A, P  Q, False